Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added eep draft for nominal types #60

Merged
merged 11 commits into from
May 20, 2024
Merged

Conversation

lucioleKi
Copy link
Contributor

This commit adds the eep draft for nominal types. I plan to make a post on Erlang forum, introducing nominal types. The post will refer to this pull request.

@kikofernandez kikofernandez self-assigned this Apr 11, 2024
@RaimoNiskanen
Copy link
Contributor

RaimoNiskanen commented Apr 18, 2024

I am missing a more formal definition for the suggested nominal types.
As it stands now I have a hard time to follow the reasoning and examples...

Such as:

A function that has a -spec that states an argument to be nominal type a/0, accepts:

  • Nominal type a/0
  • A supertype to nominal type a/0
  • A compatible structural type.
  • ¿ A subtype to nominal type a/0 ?

A function that has a -spec that it returns a nominal type b/0 may return:

  • Nominal type b/0
  • A supertype to nominal type b/0
  • A compatible structural type.
  • ¿ A subtype to nominal type b/0 ?

A function that has a -spec that states an argument to be structural type c/0, accepts:

  • A compatible structural type.
  • A nominal subtype of structural type c/0

A function that has a -spec that it returns a structural type d/0 may return:

  • A compatible structural type.
  • A nominal subtype of structural type d/0

"supertype" and "subtype" also needs to be defined, and maybe "compatible structural type"

@zuiderkwast
Copy link

That's what I though opaque types are. My interpretation of opaque types is that you can't assume anything about what they are so you need to treat them as nominal types.

Type checkers probably differ here though. I don't know what Dialyzer does.

@lucioleKi
Copy link
Contributor Author

@RaimoNiskanen It seems that my intentional avoidance of subtyping in the EEP draft causes more problems than benefits. I used 'nested nominals' instead of 'subtyping', because I wanted to emphasize that the supertypes and subtypes accepted are nominal supertypes and nominal subtypes. In Erlang, the only way to declare a nominal subtype is to declare a nested nominal of the form -nominal a() :: b() where b() is another nominal type.

I'd phrase it as follows (same for b/0):

A function that has a -spec that states an argument to be nominal type a/0, accepts:

  • Nominal type a/0

  • A nominal supertype to nominal type a/0

  • A compatible structural type.

  • A nominal subtype to nominal type a/0

@RaimoNiskanen
Copy link
Contributor

@lucioleKi, and what gives for return types?

@lucioleKi
Copy link
Contributor Author

@zuiderkwast Yes, opaque types have always been type-checked by names in Dialyzer, just with more restrictions. Dialyzer assumes no knowledge about opaque's structure, does not consider subtyping, etc. That's why the proposed nominal type-checking can cover opaque type-checking internally in Dialyzer. Nominal types are 'transparent' though. This EEP suggests a way to support nominal types and type-checking without opacity.

@lucioleKi
Copy link
Contributor Author

@RaimoNiskanen The examples c/0 and d/0 behaves as you described. For a nominal type a() :: T and a structural type S, S is a 'compatible structural type' of a() when the intersection of T and S is non-empty. (I'm not sure if this definition is too technical. This is how Dialyzer does it internally.)

A function that has a -spec that it returns a nominal type b/0 may return the following without Dialyzer raising an error:

  • Nominal type b/0

  • A nominal supertype to nominal type b/0

  • A compatible structural type.

  • A nominal subtype to nominal type b/0

@RaimoNiskanen
Copy link
Contributor

Great! I think these definitions should be in the EEP.

Copy link
Contributor

@kikofernandez kikofernandez left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this was a good addition. I have just one minor comment

eeps/eep-XXX.md Outdated
- 4711 and 42 are not structurally compatible.
- 4711 and `integer()` are structurally compatible. (Their intersection
is the value 4711.)
- `list(any_type)` and `[]` are structurally compatible.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since you write the reason, may it helps the reader if you write their intersection as in the prev. point above

@RaimoNiskanen
Copy link
Contributor

A general comment; I think the EEP should at least try to be less Dialyzer-centric.

When the text can be more generic, talk about "the type checker" and how nominals are supposed to be handled by "the type checker"; any type checker.

When talking about the implementation the text must of course talk about Dialyzer...

@kikofernandez kikofernandez merged commit 8adddb6 into erlang:master May 20, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants